The invention is generally directed to the area of verification for IC designs. In particular, some embodiments of the invention are related to an improved approach for implementing equivalence checking functionality in EDA verification tools.
Today's integrated circuits (ICs) typically contain large numbers of circuit elements. Computer-aided design (CAD) and computer-aided engineering (CAE) tools are essential in assisting circuit designers to produce these complicated ICs. Circuit designs are typically represented in a user-specified hardware description language (HDL), which demonstrate the behavioral properties of the circuit.
Designers commonly utilize CAE software, or synthesis, to translate the behavioral representation, for example, a Register-Transfer-Level (RTL) description, into an implementation representation, for example, a gate-level representation. The synthesizer chooses the implementation architecture based on parameters such as timing, footprint, and power consumption. The result of the synthesis process, the gate-level representation, is referred to as the revised circuit, while the behavioral property of the circuit, the RTL representation, is referred to as the golden circuit. The possibility of errors in creating an implementation architecture from a golden circuit is high as the process is complex.
With increasing design complexity, formal verification becomes integral in the design process to ensure that the revised circuit is equivalent to the original specification, or golden circuit. In the verification of digital circuits, signals in the circuits are “compared” in some manner in order to draw a conclusion on the “correctness” of one or more properties of the circuits. For example, to determine if two circuits with identical state encoding will behave identically under some excitations, the simulated values of the corresponding state-points in the two circuits are compared when the circuits are subjected to the same excitations.
Alternatively, to show that the two circuits will behave identically under all possible excitations, a formal methodology is used wherein the functions of the corresponding state-points in the two circuits are proved to be functionally equivalent. This method is known as formal equivalence checking and it is in the category of verification methods known as formal verification:
More specifically, during equivalence checking, an implementation architecture is created for the golden circuit and is compared to a possibly synthesized revised implementation circuit to determine if they are equivalent. However, the implementation architecture in the golden circuit is not limited by considerations of power consumption, footprint, or timing, and thus, can, and often does, choose a different architecture. The likelihood of different architectures being chosen increases when datapath components are used.
Datapath components are sub-circuits which implement arithmetic operations like multiplication, addition, squaring, shifting and division. Typically these components operate on more than one bit of data at a time. Other examples include the adder tree or partial product generator in the multiplier.
There are a great number of ways to implement a datapath component while maintaining the same functionality. There are well defined methods of implementing the datapath component at bit level to achieve specific goals like power, timing, area, placement etc. Such methods generate architectures of the datapath component. Common examples of architectures for a multiplier summation tree include ripple carry, carry save and Wallace tree. Similar architectures exist for adder, subtractors, dividers, shifters.
As such, when a datapath component exists in the golden design, the revised design may have very different architecture than the implementation version of the golden design created during equivalence checking. If the architecture generated for golden design is dramatically different from the revised architecture, then excessive system resources/runtime may be needed to perform equivalence checking of the two designs. If the architecture generated from the RTL for equivalence checking is very close to the revised gate-level implementation, then system resources/runtime that is needed to perform equivalence checking of the two designs will be minimized.
A solution is needed for equivalence checking to automatically create an implementation architecture of an RTL model that is similar to the revised gate-level implementation as possible, without relying on any external auxiliary files which annotate the revised circuit information.
A method of subcircuit architecture selection and replacement is defined in the purpose to re-generate the golden circuit which is more similar in relation to the revised circuit. The method includes creating the candidates, evaluating the candidates, selecting the best candidate, and replacing the subcircuit with the selected candidate.